package kodkod.analysis;

import java.util.*;

import edu.mit.csail.sdg.alloy4whole.AlloyBenchmark;

import kodkod.analysis.BoundsExtension.Op;
import kodkod.ast.*;
import kodkod.instance.Tuple;
import kodkod.instance.TupleFactory;
import kodkod.instance.TupleSet;
import kodkod.util.ints.IndexedEntry;
import kodkod.util.ints.IntIterator;
import kodkod.util.ints.IntSet;
import kodkod.util.ints.IntTreeSet;

public class ExpressionAnalyzer {
	
	static TupleFactory factory = null;
	static int base;
	private static HashMap<Expression, ExpressionAnalyzer> hash;
	
	public Expression expression;
	public int arity;
	
	public static double FUZZINESS = 0.001;
	
	public IntSet fuzzyUpper = new IntTreeSet();
	public IntSet fuzzyLower = new IntTreeSet();
	public int[] fuzzyMax;
	public int[] fuzzyMin;
	
	public IntSet fuzzySpan; // fuzzyUpper - fuzzyLower
	
	public HashMap<Integer, Double> plainSolutionRates = new HashMap<Integer, Double>();
	
	public final boolean TLSC = true; // only top-level special-cases (skip nested comprehensions and ifExpressions)
	ArrayList<Comprehension> comprehensions = new ArrayList<Comprehension>();
	ArrayList<IfExpression> ifExpressions = new ArrayList<IfExpression>();
	
	ArrayList<ExpressionAnalyzer> children = new ArrayList<ExpressionAnalyzer>();
	enum Op {
		NONE, RELATION, DECL, CONST, CLOSURE, REFLEXIVE_CLOSURE, TRANSPOSE, UNION, INTERSECTION, DIFFERENCE, PRODUCT, JOIN, OVERRIDE, COMPREHENSION, IFTHENELSE, PROJECTION, CAST
	}
	Op type = Op.NONE;
	
	public static ExpressionAnalyzer get(Expression e) {
		if (factory != Analyzer.translation.bounds.universe().factory()) {
			factory = Analyzer.translation.bounds.universe().factory();
			base = factory.universe().size();
			hash = new HashMap<Expression, ExpressionAnalyzer>();
		}
		
		if (hash.containsKey(e)) {
			return hash.get(e);
		} else {
			ExpressionAnalyzer rate = new ExpressionAnalyzer(e);
			if (rate.type == Op.CONST || rate.type == Op.RELATION || rate.type == Op.DECL) hash.put(e, rate);
			return rate;
		}
	}
	
	private ExpressionAnalyzer(Expression e) {
		expression = e;
		arity = e.arity();
		
		if (e instanceof LeafExpression) {
			if (e instanceof Relation) {
				type = Op.RELATION;
			} else if (e instanceof Variable) {
				if (Analyzer.translation.skolemRelations.containsKey(e)) {
					type = Op.RELATION;
					this.expression = Analyzer.translation.skolemRelations.get(e);
				} else {
					type = Op.DECL;
					children.add(ExpressionAnalyzer.get(Analyzer.initialAnalysis.decls.get((Variable)e)));
				}
			} else if (e instanceof ConstantExpression) {
				type = Op.CONST;
			}
		} else if (e instanceof UnaryExpression) {
			UnaryExpression exp = (UnaryExpression)e;
			children.add(ExpressionAnalyzer.get(exp.expression()));
			switch (exp.op()) {
				case REFLEXIVE_CLOSURE: type = Op.REFLEXIVE_CLOSURE; break;
				case CLOSURE: 	type = Op.CLOSURE; break;
				case TRANSPOSE: type = Op.TRANSPOSE; break;
			}
		} else if (e instanceof BinaryExpression) {
			BinaryExpression exp = (BinaryExpression)e;
			children.add(ExpressionAnalyzer.get(exp.left()));
			children.add(ExpressionAnalyzer.get(exp.right()));
			switch (exp.op()) {
				case DIFFERENCE: 	type = Op.DIFFERENCE; break;
				case INTERSECTION: 	type = Op.INTERSECTION; break;
				case JOIN: 			type = Op.JOIN; break;
				case OVERRIDE: 		type = Op.OVERRIDE; break;
				case PRODUCT: 		type = Op.PRODUCT; break;
				case UNION: 		type = Op.UNION; break;
			}
		} else if (e instanceof NaryExpression) {
			NaryExpression exp = (NaryExpression)e;
			for (Expression child : exp) {
				children.add(ExpressionAnalyzer.get(child));
			}
			switch (exp.op()) {
				case INTERSECTION: 	type = Op.INTERSECTION; break;
				case OVERRIDE: 		type = Op.OVERRIDE; break;
				case PRODUCT: 		type = Op.PRODUCT; break;
				case UNION: 		type = Op.UNION; break;
			}
		} else if (e instanceof Comprehension) {
			Comprehension exp = (Comprehension)e;
			for (Decl decl : exp.decls()) {
				children.add(ExpressionAnalyzer.get(decl.expression()));
			}
			type = Op.COMPREHENSION;
			comprehensions.add(exp);//
		} else if (e instanceof IfExpression) {
			IfExpression exp = (IfExpression)e;
			children.add(ExpressionAnalyzer.get(exp.thenExpr()));
			children.add(ExpressionAnalyzer.get(exp.elseExpr()));
			type = Op.IFTHENELSE;
			ifExpressions.add(exp);//
		} else if (e instanceof ProjectExpression) {
			ProjectExpression exp = (ProjectExpression)e;
			children.add(ExpressionAnalyzer.get(exp.expression()));
			type = Op.PROJECTION;
		} else if (e instanceof IntToExprCast) {
			IntToExprCast exp = (IntToExprCast)e;
			type = Op.CAST;
		}
		
		if (!TLSC || !Arrays.asList(new Op[] {Op.COMPREHENSION, Op.IFTHENELSE}).contains(this.type)) {
			for (ExpressionAnalyzer child : children) {
				this.ifExpressions.addAll(child.ifExpressions);
				this.comprehensions.addAll(child.comprehensions);
			}
		}

		fuzzyMax = new int[arity];
		fuzzyMin = new int[arity];
		initBounds();
		if (type != Op.CONST) updateFuzzyMinMax();

		IntTreeSet tuples = new IntTreeSet(fuzzyUpper);
		tuples.removeAll(fuzzyLower);
		
		IntIterator iter = tuples.iterator();
		while (iter.hasNext()) {
			int tupleIndex = iter.next();
			double solutionRate = getSolutionRate(tupleIndex);
			
			if (solutionRate >= 1 - FUZZINESS) {
				fuzzyLower.add(tupleIndex);
			} else if (solutionRate <= FUZZINESS) {
				fuzzyUpper.remove(tupleIndex);
			}
		}
		
		fuzzySpan = new IntTreeSet(fuzzyUpper);
		fuzzySpan.removeAll(fuzzyLower);
		
		if (type != Op.CONST) updateFuzzyMinMax();
	}
	
	public int nofElements() {
		return fuzzySpan.size();
	}
	
	public int extractAtom(int index, int atomIndex) {
		int trail = index / bpow(atomIndex);
		return trail % base;
	}
	
	public void updateFuzzyMinMax(int index) {
		for (int pos = 0; pos < arity; pos++) {
			int atom = extractAtom(index, pos);
			if (atom < fuzzyMin[pos]) fuzzyMin[pos] = atom;
			if (atom > fuzzyMax[pos]) fuzzyMax[pos] = atom;
		}
	}
	
	public void updateFuzzyMinMax() {
		for (int pos = 0; pos < arity; pos++) {
			fuzzyMin[pos] = base;
			fuzzyMax[pos] = 0;
		}
		IntIterator iter = fuzzyUpper.iterator();
		while (iter.hasNext()) {
			updateFuzzyMinMax(iter.next());
		}
	}
	
	private int bpow(int exp) {
		return (int)Math.pow(base, exp);
	}
	
	public void initBounds() {
		switch (this.type) {
		case RELATION:
			fuzzyUpper = Analyzer.translation.bounds.upperBound((Relation)expression).indexView();
			fuzzyLower = Analyzer.translation.bounds.lowerBound((Relation)expression).indexView();
			break;
		case CONST:
			if (expression.equals(ConstantExpression.UNIV)) {
				for (int i = 0; i < base; i++) {
					fuzzyLower.add(i);
					fuzzyUpper.add(i);
				}
				fuzzyMin[0] = 0; fuzzyMax[0] = base-1;
			} else if (expression.equals(ConstantExpression.IDEN)) {
				for (int i = 0; i < base; i++) {
					fuzzyLower.add(i*base+i);
					fuzzyUpper.add(i*base+i);
				}
				fuzzyMin[0] = 0; fuzzyMax[0] = base-1;
				fuzzyMin[1] = 0; fuzzyMax[1] = base-1;
			} else if (expression.equals(ConstantExpression.NONE)) {
				fuzzyMin[0] = base; fuzzyMax[0] = 0;
			} else if (expression.equals(ConstantExpression.INTS)) {
				fuzzyMin[0] = base; fuzzyMax[0] = 0;
				for (IndexedEntry<TupleSet> entry : Analyzer.translation.bounds.intBounds()) {
					for (Tuple t : entry.value()) {
						fuzzyLower.add(t.index());
						fuzzyUpper.add(t.index());
						updateFuzzyMinMax(t.index());
					}
				}
			}
			break;
		case DECL:
			fuzzyUpper = children.get(0).fuzzyUpper;
			fuzzyLower = children.get(0).fuzzyLower;
			fuzzyMin = children.get(0).fuzzyMin; 
			fuzzyMax = children.get(0).fuzzyMax;
			break;
		case TRANSPOSE:
			IntIterator iter = children.get(0).fuzzyUpper.iterator();
			while (iter.hasNext()) {
				int index = iter.next();
				fuzzyUpper.add(index / base + (index % base) * base);
			}
			iter = children.get(0).fuzzyLower.iterator();
			while (iter.hasNext()) {
				int index = iter.next();
				fuzzyLower.add(index / base + (index % base) * base);
			}
			break;
		case CLOSURE:
			fuzzyUpper.addAll(children.get(0).fuzzyUpper);
			fuzzyLower.addAll(children.get(0).fuzzyLower);
		case REFLEXIVE_CLOSURE: //fallthrough intended
			for (int i = 0; i < base; i++) {
				fuzzyUpper.add(i*base+i);
				fuzzyLower.add(i*base+i);
			}
			break;
		case IFTHENELSE:
		case UNION:
		case OVERRIDE:
			for (ExpressionAnalyzer child : children) {
				fuzzyUpper.addAll(child.fuzzyUpper);
				fuzzyLower.addAll(child.fuzzyLower);
			}
			break;
		case INTERSECTION:
			fuzzyUpper.addAll(children.get(0).fuzzyUpper);
			fuzzyLower.addAll(children.get(0).fuzzyLower);
			for (int i = 1; i < children.size(); i++) {
				fuzzyUpper.retainAll(children.get(0).fuzzyUpper);
				fuzzyLower.retainAll(children.get(0).fuzzyLower);
			}
			break;
		case DIFFERENCE:
			fuzzyUpper.addAll(children.get(0).fuzzyUpper);
			fuzzyLower.addAll(children.get(0).fuzzyLower);
			fuzzyUpper.removeAll(children.get(1).fuzzyLower);
			fuzzyLower.removeAll(children.get(1).fuzzyLower);
			break;
		case PRODUCT:
		case COMPREHENSION:
			IntTreeSet intermediateProduct = new IntTreeSet(children.get(0).fuzzyUpper);
			IntTreeSet product = new IntTreeSet();
			for (int i = 1; i < children.size(); i++) {
				product = new IntTreeSet();
				IntIterator iter1 = intermediateProduct.iterator();
				while (iter1.hasNext()) {
					int factor1 = iter1.next() * bpow(children.get(i).arity);
					IntIterator factor2 = children.get(i).fuzzyUpper.iterator();
					while (factor2.hasNext()) {
						product.add(factor1 + factor2.next());
					}
				}
				intermediateProduct = product;
			}
			fuzzyUpper.addAll(product);
			
			intermediateProduct = new IntTreeSet(children.get(0).fuzzyLower);
			product = new IntTreeSet();
			for (int i = 1; i < children.size(); i++) {
				product = new IntTreeSet();
				IntIterator iter1 = intermediateProduct.iterator();
				while (iter1.hasNext()) {
					int factor1 = iter1.next() * bpow(children.get(i).arity);
					IntIterator factor2 = children.get(i).fuzzyLower.iterator();
					while (factor2.hasNext()) {
						product.add(factor1 + factor2.next());
					}
				}
				intermediateProduct = product;
			}
			fuzzyLower.addAll(product);
			
			break;
		case JOIN:
			IntIterator iter1 = children.get(0).fuzzyUpper.iterator();
			while (iter1.hasNext()) {
				int index1 = iter1.next();
				int c1 = index1 % base;
				IntIterator iter2 = children.get(1).fuzzyUpper.iterator();
				while (iter2.hasNext()) {
					int index2 = iter2.next();
					int c2 = index2 / bpow(children.get(1).arity-1);
					if (c1 == c2) {
						int index = bpow(children.get(1).arity-1) * (index1 / base) + index2 % bpow(children.get(1).arity-1);
						fuzzyUpper.add(index);
					}
				}
			}
			iter1 = children.get(0).fuzzyLower.iterator();
			while (iter1.hasNext()) {
				int index1 = iter1.next();
				int c1 = index1 % base;
				IntIterator iter2 = children.get(1).fuzzyLower.iterator();
				while (iter2.hasNext()) {
					int index2 = iter2.next();
					int c2 = index2 / bpow(children.get(1).arity-1);
					if (c1 == c2) {
						int index = bpow(children.get(1).arity-1) * (index1 / base) + index2 % bpow(children.get(1).arity-1);
						fuzzyLower.add(index);
					}
				}
			}
			break;
		case PROJECTION:
			ProjectExpression exp = (ProjectExpression)expression;
			ArrayList<Integer> cols = new ArrayList<Integer>();
			for (int col = 0; col < arity; col++) {
				IntExpression intExp = exp.column(col);
				if (intExp instanceof IntConstant) {
					int column = ((IntConstant)intExp).value();
					cols.add(column);
				}
			}
			
			iter = children.get(0).fuzzyUpper.iterator();
			while (iter.hasNext()) {
				int index = iter.next();
				ArrayList<Object> list = new ArrayList<Object>();
				for (int col : cols) {
					list.add(factory.tuple(children.get(0).arity, index).atom(col));
				}
				fuzzyUpper.add(factory.tuple(list).index());
			}
			iter = children.get(0).fuzzyLower.iterator();
			while (iter.hasNext()) {
				int index = iter.next();
				ArrayList<Object> list = new ArrayList<Object>();
				for (int col : cols) {
					list.add(factory.tuple(children.get(0).arity, index).atom(col));
				}
				fuzzyUpper.add(factory.tuple(list).index());
			}
			break;
		case CAST:
			for (IndexedEntry<TupleSet> entry : Analyzer.translation.bounds.intBounds()) {
				TupleSet ts = entry.value();
				this.fuzzyUpper.addAll(ts.indexView());
				this.fuzzyLower.addAll(ts.indexView());
			}
			break;
		case NONE:
		default:
			System.err.println("Warning: Unhandled Expression Type @"+this.expression);
		}
	}
	
	public double getSolutionRate(int gateIndex) {
		if (plainSolutionRates.containsKey(gateIndex)) {
			return plainSolutionRates.get(gateIndex);
		}
		
		boolean borderCheck = true;
		for (int pos = 0; pos < arity; pos++) {
			int atom = (gateIndex / bpow(pos)) % base;
			borderCheck &= atom >= fuzzyMin[pos] && atom <= fuzzyMax[pos];
		}
		
		if (!borderCheck || !fuzzyUpper.contains(gateIndex)) {
			return 0.0;
		} else if (fuzzyLower.contains(gateIndex)) {
			return 1.0;
		}
		
		double solutionRate = 0.0;
		
		switch (this.type) {
		case RELATION:{
			solutionRate = 0.5;
			break;}
		case CONST:{
			//caught by bounds
			System.err.println("Warning: Unexpected Const @"+this.expression);
			break;}
		case DECL:{
			solutionRate = children.get(0).getSolutionRate(gateIndex);
			break;}
		case TRANSPOSE: {
			int transpose = gateIndex / base + (gateIndex % base) * base;
			solutionRate = children.get(0).getSolutionRate(transpose);
			break;}
		case REFLEXIVE_CLOSURE:
		case CLOSURE:{//unary
			solutionRate = children.get(0).getSolutionRate(gateIndex);
			break;}
		case UNION:{//nary
			solutionRate = 0.0;
			for (ExpressionAnalyzer child : children) {
				solutionRate = 1 - (1 - solutionRate) * (1 - child.getSolutionRate(gateIndex));
			}
			break;}
		case INTERSECTION:{//nary
			solutionRate = 1.0;
			for (ExpressionAnalyzer child : children) {
				solutionRate *= child.getSolutionRate(gateIndex);
			}
			break;}
		case DIFFERENCE:{//binary
			solutionRate = children.get(0).getSolutionRate(gateIndex) * (1 - children.get(1).getSolutionRate(gateIndex));
			break;}
		case PRODUCT://nary
		case COMPREHENSION:{
			solutionRate = 1.0;
			int index = gateIndex;
			int trail = arity;
			for (ExpressionAnalyzer child : children) {
				trail -= child.arity;
				solutionRate *= child.getSolutionRate(index / bpow(trail));
				index %= bpow(trail);
			}
			break;}
		case JOIN:{//binary
			ExpressionAnalyzer child0 = children.get(0);
			ExpressionAnalyzer child1 = children.get(1);
			int prefix = gateIndex / bpow(child1.arity-1);
			int suffix = gateIndex % bpow(child1.arity-1);
			
			int min = Math.min(child0.fuzzyMin[child0.arity-1], child1.fuzzyMin[0]);
			int max = Math.max(child0.fuzzyMax[child0.arity-1], child1.fuzzyMax[0]);
			
			solutionRate = 0.0;
			for (int i = min; i <= max; i++) {
				int t0 = prefix * base + i;
				int t1 = i * bpow(child1.arity-1) + suffix;
				solutionRate = 1 - (1 - solutionRate) * (1 - child0.getSolutionRate(t0) * child1.getSolutionRate(t1));
//				System.out.println(gateIndex + " t0: " + child0.expression + ": " + child0.getSolutionRate(t0));
//				System.out.println(gateIndex + " t1: " + child1.expression + ": " + child1.getSolutionRate(t1));
//				System.out.println("solutionRate: " + solutionRate);
			}
			break;}
		case OVERRIDE:{//nary
			int pos = 0;
			solutionRate = 1.0;
			for (ExpressionAnalyzer child : children) {
				solutionRate *= 1 - child.getSolutionRate(gateIndex);
				
				int power = bpow(arity-1);
				int i0 = (gateIndex / power) * power;
				for (int r = 0; pos > 0 && r < power; r++) {
					solutionRate *= Math.pow(child.getSolutionRate(i0 + r), pos);
				}
				
				pos++;
			}
			break;}
		case IFTHENELSE:{//introducing artificial or-gate between if- and else-gate
			ExpressionAnalyzer thenExpr = children.get(0);
			ExpressionAnalyzer elseExpr = children.get(1);
			solutionRate = 1 - (1 - thenExpr.getSolutionRate(gateIndex)) * (1 - elseExpr.getSolutionRate(gateIndex));
			break;}
		case PROJECTION:{
			ExpressionAnalyzer child = children.get(0);
			
			ArrayList<Integer> cols = new ArrayList<Integer>();
			for (int i = 0; i < arity; i++) {
				IntExpression intExp = ((ProjectExpression)expression).column(i);
				if (intExp instanceof IntConstant) {
					cols.add(((IntConstant)intExp).value());
				} else {
					int rand = (int)Math.floor(Math.random() * child.arity);
					System.err.println("Warning: Unable to evaluate @" + intExp + " - using " + rand);
					cols.add(rand);
				}
			}
			
			// build a (partial) tuple-index 
			int rootIndex = 0;
			ArrayList<Integer> blanks = new ArrayList<Integer>();
			Tuple tuple = factory.tuple(arity, gateIndex);
			for (int d = 0; d < child.arity; d++) {
				if (cols.contains(d)) {
					rootIndex += tuple.atomIndex(cols.indexOf(d)) * bpow(child.arity - d - 1);
				} else {
					blanks.add(bpow(child.arity - d - 1));
				}
			}
			
			// create all involved indices in case of blanks
			ArrayList<Integer> indexes = new ArrayList<Integer>();
			indexes.add(rootIndex);
			while (blanks.size() > 0) {
				int blank = blanks.remove(0);
				
				ArrayList<Integer> moreIndexes = new ArrayList<Integer>();
				for (int atom = 1; atom < base; atom++) {
					for (int i : indexes) {
						moreIndexes.add(i + blank*atom);
					}
				}
				indexes.addAll(moreIndexes);
			}
			
			// now calculate the solution-rate of the or-gate
			solutionRate = 0.0;
			for (int i : indexes) {
				solutionRate = 1 - (1 - solutionRate) * (1 - child.getSolutionRate(i));
			}
			break;}
		case CAST:
			solutionRate = 1.0;
			break;
		case NONE:
		default:
			solutionRate = 0.0;
			System.err.println("Warning: Unhandled Expression Type @"+this.expression);
		}
		
		plainSolutionRates.put(gateIndex, solutionRate);
		
		return solutionRate;
	}
	
	public DerivedSolutionRates getDerivedSolutionRates(int tupleIndex, Op[] leafs) {
		boolean borderCheck = true;
		
		for (int pos = 0; pos < arity; pos++) {
			int atom = extractAtom(tupleIndex, pos);
			borderCheck &= atom >= fuzzyMin[pos] && atom <= fuzzyMax[pos];
		}
		
		if (!borderCheck || !fuzzyUpper.contains(tupleIndex)) {
			return new DerivedSolutionRates(0.0);
		} else if (fuzzyLower.contains(tupleIndex)) {
			return new DerivedSolutionRates(1.0);
		}
		
		DerivedSolutionRates solutionRates = null;
		
		if (Arrays.asList(leafs).contains(this.type)) {
			solutionRates = new DerivedSolutionRates(0.5);
			solutionRates.newDerivedRate(expression);
			return solutionRates;
		}
		
		switch (this.type) {
		case RELATION:{
			solutionRates = new DerivedSolutionRates(0.5);
			break;}
		case CONST:{
			//caught by bounds
			System.err.println("Warning: Unexpected Const @"+this.expression);
			break;}
		case DECL:{
			solutionRates = children.get(0).getDerivedSolutionRates(tupleIndex, leafs);
			break;}
		case TRANSPOSE: {
			int transpose = tupleIndex / base + (tupleIndex % base) * base;
			solutionRates = children.get(0).getDerivedSolutionRates(transpose, leafs);
			break;}
		case CLOSURE:{//unary
			solutionRates = children.get(0).getDerivedSolutionRates(tupleIndex, leafs);
			break;}
		case UNION:{//nary
			solutionRates = new DerivedSolutionRates(0.0);
			for (ExpressionAnalyzer child : children) {
				solutionRates.or(child.getDerivedSolutionRates(tupleIndex, leafs));
			}
			break;}
		case INTERSECTION:{//nary
			solutionRates = new DerivedSolutionRates(1.0);
			for (ExpressionAnalyzer child : children) {
				solutionRates.and(child.getDerivedSolutionRates(tupleIndex, leafs));
			}
			break;}
		case DIFFERENCE:{//binary
			solutionRates = children.get(0).getDerivedSolutionRates(tupleIndex, leafs);
			solutionRates.and(children.get(1).getDerivedSolutionRates(tupleIndex, leafs).not());
			break;}
		case COMPREHENSION:
			FormulaAnalyzer fa = new FormulaAnalyzer(((Comprehension)expression).formula(), false);
			double penalty = fa.getSolutionRate();
			solutionRates = new DerivedSolutionRates(penalty);
			// fall-through:
		case PRODUCT: { //nary 
			if (solutionRates == null) 
				solutionRates = new DerivedSolutionRates(1.0);
			int index = tupleIndex;
			int trail = arity;
			for (ExpressionAnalyzer child : children) {
				trail -= child.arity;
				solutionRates.and(child.getDerivedSolutionRates(index / bpow(trail), leafs));
				index %= bpow(trail);
			}
			break;}
		case JOIN:{//binary
			ExpressionAnalyzer child0 = children.get(0);
			ExpressionAnalyzer child1 = children.get(1);
			int prefix = tupleIndex / bpow(child1.arity-1);
			int suffix = tupleIndex % bpow(child1.arity-1);
			
			int min = Math.min(child0.fuzzyMin[child0.arity-1], child1.fuzzyMin[0]);
			int max = Math.max(child0.fuzzyMax[child0.arity-1], child1.fuzzyMax[0]);
			
			solutionRates = new DerivedSolutionRates(0.0);
			for (int i = min; i <= max; i++) {
				int t0 = prefix * base + i;
				int t1 = i * bpow(child1.arity-1) + suffix;
				solutionRates.or(child0.getDerivedSolutionRates(t0, leafs).and(child1.getDerivedSolutionRates(t1, leafs)));
			}
			break;}
		case OVERRIDE:{//nary
			int pos = 0;
			solutionRates = new DerivedSolutionRates(1.0);
			for (ExpressionAnalyzer child : children) {
				solutionRates.and(child.getDerivedSolutionRates(tupleIndex, leafs).not());
				
				int power = bpow(arity-1);
				int i0 = (tupleIndex / power) * power;
				for (int r = 0; pos > 0 && r < power; r++) {
					solutionRates.and(child.getDerivedSolutionRates(i0 + r, leafs).pow(pos));
				}
				
				pos++;
			}
			break;}
		case IFTHENELSE:{
			ExpressionAnalyzer thenExpr = children.get(0);
			ExpressionAnalyzer elseExpr = children.get(1);
			//introducing artificial or-gate between if- and else-gate
			solutionRates = thenExpr.getDerivedSolutionRates(tupleIndex, leafs).or(elseExpr.getDerivedSolutionRates(tupleIndex, leafs));
			break;}
		case PROJECTION:{
			ExpressionAnalyzer child = children.get(0);
			
			ArrayList<Integer> cols = new ArrayList<Integer>();
			for (int i = 0; i < arity; i++) {
				IntExpression intExp = ((ProjectExpression)expression).column(i);
				if (intExp instanceof IntConstant) {
					cols.add(((IntConstant)intExp).value());
				} else { // should not be hit
					System.err.println("Warning: Unable to evaluate @" + intExp + " - using random column");
					cols.add((int)Math.floor(Math.random() * child.arity));
				}
			}
			
			// build a (partial) tuple-index
			int rootIndex = 0;
			ArrayList<Integer> blanks = new ArrayList<Integer>();
			for (int pos = 0; pos < child.arity; pos++) {
				if (cols.contains(pos)) {
					rootIndex += extractAtom(tupleIndex, arity - 1 - cols.indexOf(pos)) * bpow(child.arity - pos - 1);
				} else {
					blanks.add(pos);
				}
			}
			
			// create all involved indices in case of blanks
			ArrayList<Integer> indexes = new ArrayList<Integer>();
			indexes.add(rootIndex);
			while (blanks.size() > 0) {
				int blank = blanks.remove(0);
				
				ArrayList<Integer> moreIndexes = new ArrayList<Integer>();
				for (int atom = 1; atom < base; atom++) {
					for (int i : indexes) {
						moreIndexes.add(i + blank*atom);
					}
				}
				indexes.addAll(moreIndexes);
			}
			
			// now calculate the solution-rate of the or-gate
			solutionRates = new DerivedSolutionRates(0.0);
			for (int i : indexes) {
				solutionRates.or(child.getDerivedSolutionRates(i, leafs));
			}
			break;}
		case CAST:
			solutionRates = new DerivedSolutionRates(1.0);
			break;
		case NONE:
		default:
			solutionRates = new DerivedSolutionRates(0.0);
			System.err.println("Warning: Unhandled Expression Type @"+this.expression);
		}
		
		return solutionRates;
	}
	
	public HashMap<Expression, Double> getDominanceVector(int gateIndex, Op[] leafs) {
		HashMap<Expression, Double> dominances = new HashMap<Expression, Double>();
		DerivedSolutionRates derivedSolutionRates = getDerivedSolutionRates(gateIndex, leafs);
		// initialize
		for (DerivedSolutionRates.DerivedRate rate : derivedSolutionRates.derivedRates) {
			dominances.put((Expression)rate.owner, 0.0);
		}
		// sum
		for (DerivedSolutionRates.DerivedRate derivedRate : derivedSolutionRates.derivedRates) {
			double dominance = 2 * Math.abs(derivedRate.value - derivedSolutionRates.plainRate.value);
			dominances.put((Expression)derivedRate.owner, dominances.get(derivedRate.owner) + dominance);
		}
		
		return dominances;
	}
	
	public HashMap<Relation, Double> getRelationDominances() {
		HashMap<Relation, Double> dominance = new HashMap<Relation, Double>();
		
		IntIterator iter = fuzzySpan.iterator();
		while (iter.hasNext()) { //sum
			HashMap<Expression, Double> dominanceVector = this.getDominanceVector(iter.next(), new Op[] {Op.RELATION});
			
			for (Expression r : dominanceVector.keySet()) {
				if (dominance.containsKey((Relation)r)) {
					dominance.put((Relation)r, dominance.get((Relation)r) + dominanceVector.get(r));
				} else {
					dominance.put((Relation)r, dominanceVector.get(r));
				}
			}
		}

		for (Relation r : dominance.keySet()) { //average
			dominance.put(r, dominance.get(r) / BoundsExtension.get(r).size());
		}
		
		return dominance;
	}
	
	public HashMap<Comprehension, Double> getComprehensionDominances() {
		HashMap<Comprehension, Double> dominance = new HashMap<Comprehension, Double>();

		IntIterator iter = fuzzySpan.iterator();
		while (iter.hasNext()) { //sum
			HashMap<Expression, Double> dominanceVector = this.getDominanceVector(iter.next(), new Op[] {Op.COMPREHENSION});
			
			for (Expression exp : dominanceVector.keySet()) {
				if (dominance.containsKey((Comprehension)exp)) {
					dominance.put((Comprehension)exp, dominance.get((Comprehension)exp) + dominanceVector.get(exp));
				} else {
					dominance.put((Comprehension)exp, dominanceVector.get(exp));
				}
			}
		}

		for (Comprehension comp : dominance.keySet()) { //average
			dominance.put(comp, dominance.get(comp) / BoundsExtension.get(comp).size());
		}
		
		return dominance;
	}
	
	public HashMap<IfExpression, Double> getIfExpressionDominances() {
		HashMap<IfExpression, Double> dominance = new HashMap<IfExpression, Double>();

		IntIterator iter = fuzzySpan.iterator();
		while (iter.hasNext()) { //sum
			HashMap<Expression, Double> dominanceVector = this.getDominanceVector(iter.next(), new Op[] {Op.IFTHENELSE});
			
			for (Expression exp : dominanceVector.keySet()) {
				if (dominance.containsKey((IfExpression)exp)) {
					dominance.put((IfExpression)exp, dominance.get((IfExpression)exp) + dominanceVector.get(exp));
				} else {
					dominance.put((IfExpression)exp, dominanceVector.get(exp));
				}
			}
		}

		for (IfExpression ite : dominance.keySet()) { //average
			dominance.put(ite, dominance.get(ite) / BoundsExtension.get(ite).size());
		}
		
		return dominance;
	}
}
